; COMMAND-LINE:
; EXPECT: sat
(set-logic ALL)
(set-option :incremental false)
(set-option :produce-models true)
(set-option :finite-model-find true)
(declare-fun f ((_ BitVec 2) (_ BitVec 2)) (Array Int Int))
(declare-fun f0 ((_ BitVec 2)) (Array Int Int))
(declare-fun td () (Array Int Int))
(declare-fun td1 () (Array Int Int))
(declare-fun td2 () (Array Int Int))
(assert (= td1 (store td 0 1)))
(assert (= td2 (store td 0 2)))
(assert (= (f #b01 #b00) td1))
(assert (= (f #b10 #b00) td2))
(assert (= (f0 #b00) (f #b00 #b00)))
(assert (= (f0 #b01) (f #b00 #b01)))
(assert (= (f0 #b10) (f #b00 #b10)))
(assert (= (f0 #b11) (f #b00 #b11)))
(assert (forall ((i (_ BitVec 2))) (= (f0 i) td2)))
(check-sat)
